package com.googlecode.kipler.container.dl;

import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import com.googlecode.kipler.common.Copyable;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.Formula;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class PBox implements Copyable<PBox>, FormulaBase {
	private FormulaCategorizer categorizer = new FormulaCategorizer();

	private boolean isSatisfiable = true;

	public boolean isSatisfiable() {
		return isSatisfiable;
	}

	public void add(Formula formula) throws UnsatisfiableException {
		categorizer.add(formula);
		if (causesUnsatisfiability(formula)) {
			isSatisfiable = false;
			throw new UnsatisfiableException();
		}
	}

	public boolean contains(Formula formula) {
		return categorizer.contains(formula);
	}

	/**
	 * @param conDef
	 * @throws UnsatisfiableException
	 */
	private boolean causesUnsatisfiability(Formula formula) {
		boolean result = true;
		Formula negFormula = formula.copy().toggleNegated();
		if (!categorizer.contains(negFormula)) {
			result = false;
		}
		return result;
	}

	public Set<Formula> getFormulas() {
		Set<Formula> result = new HashSet<Formula>();
		Iterator<Formula> fIter = categorizer.formulaIterator();
		while (fIter.hasNext()) {
			Formula f = fIter.next();
			result.add(f);
		}
		return result;
	}

	public Iterator<Formula> formulaIterator(FormulaCategory cat) {
		return categorizer.categoryIterator(cat);
	}

	public PBox copy() {
		PBox pbox = new PBox();
		pbox.isSatisfiable = isSatisfiable;
		pbox.categorizer = categorizer.copy();
		return pbox;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			PBox other = (PBox) obj;
			return this.size() == other.size()
					&& categorizer.equals(other.categorizer);
		}
		return false;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append("PBox");
		buffer.append(" = {");
		for (Formula f : getFormulas())
			buffer.append(f + ", ");
		buffer.delete(buffer.length() - 2, buffer.length());
		buffer.append("}");
		return buffer.toString();
	}

	public int size() {
		return categorizer.size();
	}

}
